
#ifndef NODE_H
#define NODE_H

struct Node;

#include <fstream>
#include <vector>
#include <list>
#include <math.h>
#include "ProblemData.h"

using namespace std;

class Node
{
public:
	Node():bitmap(NULL), nb_unaffected(NULL), selectedVars(NULL){}
	Node(int a_n, int a_m);
	Node(const Node &node);
	Node(char *b, size_t * u, int a_n, int a_m);
	~Node();
	void printSolution();

	/**
	 * Write the solution to a file in CNF DIMACS format.
	 *
	 * @param file_name The path to file in which to write the solution.
	 */
	void writeSolution(string file_name);

	vector<Node> explore(unsigned int N);
	vector<Node> exploreParallel(unsigned int N);

	static Node getFirstNode(ProblemData data);
	static Node exploreOne(char* b, size_t * u, int *vars, int n, int m, int N, int i);
	
	inline int unaffected(int N)
	{
		delete[] selectedVars;
		
		selectedVars = new int[N];
		int counter = 0;
		
		for(int i=0; i<n && counter < N; i++)
		{
			if(!varAffected(i))
			{
				selectedVars[counter]=i;
				counter++;
			}
		}
		
		nbSelected = counter;
		return(nbSelected);
	}
	
	inline bool isSolved() const
	{
		return *(bitmap) & (1 << 0);
	}
	
	inline bool isSolvable() const
	{
		return *(bitmap) & (1 << 1);
	}
	
	inline bool varAffected(int i) const
	{
		return *(b1 + i / 8) & (1 << i % 8);
	}
	
	inline bool varValues(int i) const
	{
		return *(b2 + i / 8) & (1 << i % 8);
	}
	
	inline bool solvedClauses(int i) const
	{
		return *(b3 + i / 8) & (1 << i % 8);
	}
	
	inline bool clauseLiterals(int k, int i) const
	{
		return *(b4 + (k + i * m) / 8) & (1 << (k + i * m) % 8);
	}

	inline void set_solved(bool val)
	{
		if (isSolved() != val)
		{
			*(bitmap) ^= (1 << 0);
		}
	}
	
	inline void set_solvable(bool val)
	{
		if (isSolvable() != val)
		{
			*(bitmap) ^= (1 << 1);
		}
	}
	
	inline void set_varAffected(int i, bool val)
	{
		if (varAffected(i) != val)
		{
			*(b1 + i / 8) ^= (1 << i % 8);
		}
	}
	
	inline void set_varValues(int i, bool val)
	{
		if (varValues(i) != val)
		{
			*(b2 + i / 8) ^= (1 << i % 8);
		}
	}
	
	inline void set_solvedClauses(int i, bool val)
	{
		if (solvedClauses(i) != val)
		{
			*(b3 + i / 8) ^= (1 << i % 8);
		}
	}
	
	inline void set_clauseLiterals(int k, int i, bool val)
	{
		if (clauseLiterals(k, i) != val)
		{
			*(b4 + (k + i * m) / 8) ^= (1 << (k + i * m) % 8);
		}
	}
	
private:
	char *bitmap, *b1, *b2, *b3, *b4;
	size_t * nb_unaffected;
	int n, m, o;
	int nbSelected;
	int *selectedVars;
	size_t allocated_size;

	/**
	 * Get the index of the negation of a given literal.
	 *
	 * @param i The index of the literal to consider.
	 * @return The index corresponding to the negation of the given literal.
	 */
	inline int negation (int i) const
	{
		return 2 * n - 1 - i;
	}

	/**
	 * Perform the initial tautologies elimination (clauses which contain both a
	 * variable and its negation).
	 *
	 * @param data A reference to the data of the problem.
	 * @return The number of clauses that were eliminated.
	 */
	int init_tautologies_elimination (ProblemData & data);

	/**
	 * Perform the initial unit propagation (affect literals that appear as
	 * singles literals in a clause to true).
	 *
	 * @param data A reference to the data of the problem.
	 * @return The number of unit propagations that were performed.
	 */
	int init_unit_propagation (ProblemData & data);
	
	/**
	 * Perform the initial pure literals elimination (literals which appear in
	 * only one form in the formula, either positive or negative).
	 *
	 * @param data A reference to the data of the problem.
	 * @return The number of pure literal eliminations that were performed.
	 */
	int init_pure_literals_elimination (ProblemData & data);
};


#endif
